
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "datatypes/bool.ma".
include "structures.ma".

record CommMonoid: Type ≝ {
  phases:> setoid;
  unit: phases;
  op: phases × phases ⇒ phases;
  associative: ∀x,y,z. op x (op y z) = op (op x y) z;
  commutative: ∀x,y. op x y = op y x;
  neutral: ∀x. op unit x = x
}.

interpretation "unit" 'neutral = (unit ?). (* ⅇ *)

notation "hvbox(a break ⋆ b)"
  left associative with precedence 50 for @{ 'op $a $b }.
interpretation "op" 'op a b = (fun2 ??? (op ?) a b).

definition BOOL: CommMonoid.
 constructor 1
  [ constructor 1
     [ apply bool
     | constructor 1
        [ apply (λb1,b2:bool. b1 =_\ID b2)
        | normalize; autobatch
        | normalize; autobatch
        | normalize; autobatch ]]
  | normalize; apply true
  | constructor 1; normalize
     [ apply andb
     | intros; autobatch]
  | simplify; intros; cases x; simplify; autobatch
  | simplify; intros; cases x; cases y; autobatch
  | simplify; autobatch ]
qed.

(* LR: Proving the following theorem is "mandatory".
       The reason is that orb_assoc is missing in 
       datatypes/bool.ma and it makes point 3 in BOOLOR
       here below working. The proof "copies" the one
       of theorem andb_assoc in datatypes/bool.ma *)
theorem orb_assoc: ∀ A,B,C:bool.
(A ∨ (B ∨ C)) =_\ID ((A ∨ B) ∨ C).
intros; elim A; elim B; elim C; simplify; reflexivity.
qed.

(* Generating a commutative monoid on the setoid whose seed is 
   false and the operation is boolean or *)
definition BOOLOR: CommMonoid.
 constructor 1
  [ constructor 1
     [ apply bool
     | constructor 1
     
        [ apply (λb1,b2:bool. b1 =_\ID b2)
        | normalize; autobatch
        | normalize; autobatch
        | normalize; autobatch ]]
  | normalize; apply false
  | constructor 1; normalize
     [ apply orb
     | intros; autobatch]
  | simplify; intros; cases x; simplify; autobatch
  | simplify; intros; cases x; cases y; autobatch
  | simplify; autobatch ]
qed.

definition FreeCommMonoid: CommMonoid.
 constructor 1
  [ constructor 1
     [ apply Formula
     | constructor 1
        [ apply (λF,G. EqRelFormula F G);
        | whd; simplify; intros;
          apply EqFormula_is_Refl
        | whd; simplify; intros;
          apply EqFormula_is_Symm; assumption
        | whd; simplify; intros; apply (EqFormula_is_Tran ? y ?)
          [ assumption | assumption ]
        ]]
  | normalize; apply 𝟙
  | constructor 1; simplify
     [ apply Times
     | intros; apply (EqRelFormula_is_CntCopLR a a' b b'); autobatch ]
  | whd; simplify; intros;
    apply (Times_is_Assoc ???)
  | simplify; intros; apply (Times_is_Symm ??)
  | simplify; intros; apply (Times_has_Unit ?) ]
qed.
